\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it knd}$:Knd, $T$:Type, $l$:IdLnk, ${\it dt}$:fpf(Id; $x$.Type),\+
\\[0ex]$g$:((${\it tg}$:Id $\times$ (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$(decl{-}type\{i:l\}(${\it dt}$; ${\it tg}$) List))) List).
\-\\[0ex]Rsends(${\it ds}$; ${\it knd}$; $T$; $l$; ${\it dt}$; $g$) $\in$ es\_realizer\{i:l\}
\end{tabbing}